\begin{tabbing}
$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $f$:(E($X$)$\rightarrow$E($X$)).
\\[0ex]($\forall$$x$:E($X$). $f$($x$) c$\leq$ $x$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$, ${\it e'}$:E($X$).\+
\\[0ex](${\it e'}$ $\in$ prior{-}$f${-}fixedpoints($e$))
\\[0ex]$\Rightarrow$ ($\neg$(${\it e'}$ = $f$$\ast\ast$($e$) $\in$ E))
\\[0ex]$\Rightarrow$ ($\neg$($f$$\ast\ast$($e$) $\in$ prior{-}$f${-}fixedpoints(${\it e'}$))))
\-
\end{tabbing}